(set-logic QF_BV)
(declare-fun _substvar_3806_ () (_ BitVec 8))
(declare-fun _substvar_4053_ () (_ BitVec 8))
(declare-fun _substvar_4056_ () (_ BitVec 8))
(declare-fun _substvar_4515_ () (_ BitVec 8))
(declare-fun _substvar_4629_ () (_ BitVec 8))
(declare-fun _substvar_4719_ () (_ BitVec 8))
(declare-fun _substvar_4786_ () (_ BitVec 1))
(declare-fun _substvar_4842_ () (_ BitVec 8))
(declare-fun a () (_ BitVec 8))
(declare-fun d () (_ BitVec 8))
(assert (let ((?v_48 (_ bv0 8)) (?v_44 (= (_ bv1 1) (bvnot (ite (= (bvand _substvar_4515_ (ite (= (_ bv1 1) (bvnot (ite (= (bvand a (bvlshr (concat (_ bv1 1) (_ bv0 7)) ((_ zero_extend 5) (_ bv1 3)))) (_ bv0 8)) (_ bv1 1) (_ bv0 1)))) _substvar_4053_ (_ bv0 8))) (_ bv0 8)) (_ bv1 1) (_ bv0 1)))))) (let ((?v_63 (ite ?v_44 (_ bv0 8) a)) (?v_65 (ite ?v_44 (ite (= (_ bv1 1) (bvnot (ite (= (bvand a (bvlshr (concat (_ bv1 1) (_ bv0 7)) ((_ zero_extend 5) (_ bv1 3)))) (_ bv0 8)) (_ bv1 1) (_ bv0 1)))) _substvar_4053_ (_ bv0 8)) (_ bv0 8))) (?v_60 ((_ zero_extend 5) (_ bv1 3)))) (let ((?v_78 (bvand (bvnot ?v_65) ((_ zero_extend 5) (_ bv1 3)))) (?v_74 false)) (let ((?v_79 (ite ?v_44 (_ bv0 8) a)) (?v_80 (ite (= (_ bv1 1) (bvnot (ite (= (bvand (ite ?v_44 (_ bv0 8) a) ((_ zero_extend 5) (_ bv1 3))) (_ bv0 8)) (_ bv1 1) (_ bv0 1)))) (ite (= (_ bv1 1) (bvnot (ite (bvult d ?v_78) (_ bv1 1) (_ bv0 1)))) ?v_78 ?v_65) ?v_65)) (?v_87 (_ bv0 8)) (?v_82 (ite (= (bvand (bvand (bvnot a) d) (concat (_ bv1 1) (_ bv0 7))) (_ bv0 8)) (_ bv1 1) (_ bv0 1)))) (let ((?v_84 (bvnot ?v_82)) (?v_86 (_ bv0 1)) (?v_88 (bvnot d))) (let ((?v_141 (ite (= (_ bv1 1) (bvnot (ite (= (bvand (bvnot (ite (= (_ bv1 1) (bvnot (bvnot ?v_82))) ?v_88 (ite (= (_ bv1 1) ?v_82) (_ bv0 8) ?v_88))) (bvlshr (concat (_ bv1 1) (_ bv0 7)) ((_ zero_extend 5) (_ bv1 3)))) (_ bv0 8)) (_ bv1 1) (_ bv0 1)))) _substvar_4056_ a)) (?v_132 (_ bv0 1)) (?v_135 (_ bv0 1))) (let ((?v_197 (_ bv0 8)) (?v_188 (ite (bvult (bvnot a) (_ bv1 8)) (_ bv1 1) (_ bv0 1))) (?v_191 (bvnot (ite (bvult d (bvnot (_ bv0 8))) (_ bv1 1) (_ bv0 1))))) (let ((?v_225 (ite (= (_ bv1 1) (bvand (ite (= (ite (= (_ bv1 1) (ite (bvult (bvnot a) _substvar_4629_) (_ bv1 1) (_ bv0 1))) _substvar_4629_ (_ bv0 8)) (_ bv0 8)) (_ bv1 1) (_ bv0 1)) (bvnot (ite (bvult d (bvnot (_ bv0 8))) (_ bv1 1) (_ bv0 1))))) (ite (= (_ bv1 1) (bvnot ?v_188)) (_ bv0 8) _substvar_4842_) (_ bv0 8))) (?v_220 (ite (bvult (bvnot a) _substvar_3806_) (_ bv1 1) (_ bv0 1))) (?v_217 (_ bv0 8))) (not (= (bvand _substvar_4786_ (bvnot (ite (= (bvand (bvnot (bvand (bvnot ?v_79) (bvnot ?v_80))) (bvnot (bvand ?v_79 ?v_80))) (bvnot (bvand (bvnot (bvand ?v_141 (ite (= (_ bv1 1) (bvnot (bvnot ?v_82))) ?v_88 (ite (= (_ bv1 1) ?v_82) (_ bv0 8) ?v_88)))) (bvnot (ite (= (_ bv1 1) (bvnot (bvand ?v_220 (ite (bvult (bvnot a) _substvar_4719_) (_ bv1 1) (_ bv0 1))))) ?v_225 (_ bv0 8)))))) (_ bv1 1) (_ bv0 1)))) (_ bv0 1))))))))))))
(check-sat)
(exit)
